secret{-}table($T$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$K$:$\mathbb{N}$ $\times$ (:$\mathbb{N}$ $\times$ (\{0..$K$$^{-}$\}$\rightarrow$(:Atom1 $\times$ (:($\mathbb{N}$ + Atom1) $\times$ data($T$)))))